
\documentclass[runningheads]{llncs}
\usepackage{stmaryrd}
\usepackage{amsfonts}

\usepackage{amssymb}
\setcounter{tocdepth}{3}
\usepackage{graphicx}
\usepackage{algorithmic, algorithm}

\usepackage{url}
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{Use Coq to Model and Verify PLC Applications}

% a short form should be given in case it is too long for the running head
\titlerunning{Use Coq to Model and Verify PLC Applications}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{}
%
\authorrunning{}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{}

\toctitle{} \tocauthor{} \maketitle


\begin{abstract}



\keywords{PLC, Coq, Model Checking, Timer}
\end{abstract}

\section{Introduction}

\section{Coq and PLC}

Coq is a proof assistant based on type theory\cite{CoqArt}. Coq

\section{Quiz Machine}

Quiz machine is an equipment used in a contest. The host uses it to
reset and start a contest. After the host starts a contest, the
first player who presses his button has the chance to answer the
question. If more than one players press the button at the same
time, the machine should inform the host to restart another contest.
If during the predefined time there is no one pressing the button,
the machine should inform the host that time is out and forbid the
players to press the buttons again.

There are several properties (requirements) needed to be verified,
all of which contain the notion of time:

\begin{itemize}

\item First the host presses the reset button and after a while he presses
the start button. Between the time he presses the start button and
time-out, the light of the first player who presses his button will
be turned on and the other lights stay off.

\item First the host presses the reset button and after a while he presses
the start button. Between the time he presses the start button and
time-out, if more than one players press their buttons at the same,
their lights will be turned on and the other lights stay off. The
situation that more than one light are on indicates that there are
more than one players press buttons at the same time.

\item First the host presses the reset button and after a while he presses
the start button. Between the time he presses the start button and
time-out, if no one presses his button, the time-out light will be
turned on and the other lights stay off.

\end{itemize}

These three properties describe three typical processes that one can
meets in a quiz game. In other words, they cover all the possible
cases that may happen between the time the host presses the start
button and time-out:\begin{itemize}

\item No one presses button during that interval.

\item Only one firstly presses button during that interval.

\item More than one players press button during that interval.

\end{itemize}In that sense, they are the complete specification of the quiz
machine.

Based on the above requirements, the ladder diagram implementation
of quiz machine is shown in figure \ref{fig1_ld_quizmachine}.

\begin{figure}[]
        \center{\includegraphics[scale=0.6]
        {figs/fig1_quizmachine}}
        \caption{\label{fig1_ld_quizmachine} The LD of quiz machine}
      \end{figure}

$i0$,$i1$,$i2$ and $i3$ denotes the start button, the reset button,
player 1's button, player 2's button, and player 3's button
respectively. $t1$ is a TON-timer with time base of $100ms$. $o0$,
$o1$, $o2$, and $o3$ are the lights indicating time-out, player 1,
player 2, and player 3 respectively. $m1~m5$ represent the system's
inner states: $m1$ is ON means the machine is started, $m2$ is ON
means player 1 gets the chance, and so are $m3$ and $m4$. $m5$ is
used to record that there is already some one pressed his button
which can invalidate other's buttons.


\section{Modeling Quiz Machine}

Based on the example introduced in the previous section, we describe
how to model this example application in Coq. Intuitively, the
computation phase of each cycle is understood as a black box. It is
the inputs and outputs of this black box that we concern. The output
for the same input should be the same, since we want our model to be
deterministic. If they are different, based on our formalism
inconsistence will be introduced into our model which is not
allowed. In the following sections, we show the main steps of
modeling a PLC program in Coq.

\subsection{Cyclical Behavior and Relays}

As mentioned in the previous section, PLC has a cyclical behavior.
During each cycle it reads the inputs from the environment, does the
computations and sets the output through which it effects the
outside world. Hence, we can index these cycles based on the time
order using natural numbers:

\begin{verbatim}
Definition Cycle := nat.
\end{verbatim}

The values (i.e. ON or OFF) of relays change according to the
cycles. In other words, they are the functions from $Cycle$ to
boolean:

\begin{verbatim}
Definition Var := Cycle -> bool.
\end{verbatim}

Since the Coq system is a system based on intuitive logic, the
results of logic computation are in sort $Prop$. In order to ease
the proof process, we use the following definition instead:
\begin{verbatim}
Definition Var := Cycle -> Prop.
\end{verbatim}
If we have a relay $r$ of type $Var$, then we use $r(pred ~i)$ and
$r(i)$ to denote the values of relay $r$ at the beginning and the
end of cycle $i$ respectively.

\subsection{The Order of Instructions}

We need take into account the order of instructions and find ways to
express this order in the black box. For example, in figure
\ref{fig1_ld_quizmachine} the output $m4$ of the fifth rung depends
on the output $m5$ of the sixth rung and vice versa. Since the
ladder diagram are executed from left to right and then from up to
down, we know that in the current cycle, the value of $m4$ is
calculated before the calculation of $m5$. That is to say the value
of $m4$ which is used to compute the value of $m5$ is the value of
$m4$ in the same cycle while the value of $m5$ which is used to
compute the value of $m4$ is the value of $m5$ in the previous
cycle. We use the following Coq codes to express these two
instructions:

\begin{verbatim}
Hypothesis h_m4 : forall c, m4 c = (((m1 c /\ ~ t1 c /\ i4 c /\ ~ m5
(pred c)) \/ m4 (pred c)) /\ m1 c).

Hypothesis h_m5 : forall c, m5 c = (((m2 c \/ m3 c \/ m4 c) \/ m5
(pred c)) /\ m1 c).
\end{verbatim}

Note that we use $m4~(pred~c)$ to denote the value of $m4$ in the
previous cycle of cycle $c$. These hypothesis build the dependence
of instructions. From these dependence we know the order of
instructions: if a variable $v_1$ depends on the previous value of
another variable $v_2$ then the instruction used to compute $v_2$ is
before the that of $v_1$; if a variable $v_1$ depends on the current
value of another variable $v_2$ then the instruction used to compute
$v_1$ is before that of $v_2$.

\subsection{Assignments}

The translation of assignments to Coq is very straightforward.
Taking the order of instructions into account, the last rung in
figure \ref{fig1_ld_quizmachine} is modeled as the following:

\begin{verbatim}
Hypothesis h_o0 : forall c, o0 c = (t1 c /\ ~ m5 c).
\end{verbatim}

\subsection{RS flip-flop and SR flip-flop}

The behavior of RS and SR flip-flops are shown in table
1\cite{s7-200-manual}. The first letter of each kind of flip-flops
presents the input point which dominate the output when both point
are 1.

\begin{table}
\caption{RS flip-flop and SR flip-flop}
\begin{center}
\begin{tabular}{c c| c |c}
\hline R & S & RS flip-flop & SR flip-flop \\

\hline 0& 0& the previous value& the previous value \\
0 & 1 & 1 & 1\\
1 & 0 & 0 & 0\\
1 & 1 & 0 & 1\\
\hline

\end{tabular}
\end{center}
\end{table}

The behaviors of the following ladder diagrams (shown in figure
\ref{fig2_RS_SR}) built from only logic connections are equivalent
to RS and SR flip-flops respectively (assuming that $r$, $s$ and $m$
are the reset, set and output point of flip-flop respectively).

\begin{figure}[]
        \center{\includegraphics[scale = 0.7]
        {figs/fig2_RS_SR}}
        \caption{\label{fig2_RS_SR} Equivalent LD of RS and SR flip-flops}
      \end{figure}


These ladder diagrams can be translated to the following Coq codes:

\begin{verbatim}
Hypothesis h_m_RS : forall c, m c = ((s c \/ m (pred c)) /\ ~ r c).

Hypothesis h_m_SR : forall c, m c = ((~ r c /\ m (pred c)) \/ s c).
\end{verbatim}

\subsection{Modeling Timers}
\label{model_timer_section}

The use of timers in PLC introduces the notion of time into PLC
applications which makes the analysis more complex. In this paper,
we only consider TON-timers. A typical TON-timer and its behavior
are demonstrated in figure \ref{fig3_ton_timer}. In practice, the
behaviors of TON-timers varies from the time base chosen. Take the
timer of S7-200 for example, if we choose the TON-timer with time
base of $100ms$, the timer is only updated when the timer
instruction is executed. If we choose the TON-timer with time base
of $10ms$, the timer is updated at the beginning of each scan
cycle\cite{s7-200-manual}. Since our abstraction of the computation
phase is a black box, it is hard to model these differences. An
abstract TON-timer is needed to abstract away these differences.

\begin{figure}[]
        \includegraphics[scale = 0.5]
        {figs/fig3_ton_timer}
        \caption{\label{fig3_ton_timer} TON timer and its behivour}
      \end{figure}

An abstract timer has the following property:

\begin{itemize}

\item There is at most one point to access the value of the each timer.
In other words, we want to make sure that the changes of the value
of a timer won't affect the final outputs.

\end{itemize}

Given the LD program in figure \ref{fig1_ld_quizmachine}, it is can
be verified that the timer $t1$ satisfies the above property:

\begin{itemize}

\item $t1$ is executed one and only one in each cycle.

\item Since $t1$ is a TON-timer with time base of $100ms$, it can be
updated only when it is executed. Because $t1$ is executed only
once, its timer bit is updated only once.

\end{itemize}

Three axioms can be used to model the abstract TON-timer. We use
$t1$ to illustrate the use of these axioms, since we have already
known that $t1$ is an abstract TON-timer:

\begin{verbatim}
Definition Time := nat.

Variable f : Cycle -> Time.

Variables t1_value : Time.

Hypothesis t1_LargerThan0 :
    1 <= t1_value.

Hypothesis f_monotonic : forall c, f c < f (S c).

Hypothesis f_TimerLargerThanCycleInterval :
                    forall c, f (S c) -  f c < t1_value.

Variable t1 : Var.

Axiom h_t1_reset : forall c, ~ m1 c -> ~ t1 c.

Axiom h_t1_set :
    forall c1, forall c2, t1_value <= f c2 - f c1
        -> being_true m1 c1 c2 -> t1 c2.

Axiom h_t1_true :
    forall c2, t1 c2 -> exists c1, t1_value <= f c2 - f c1
        /\ being_true m1 c1 c2.
\end{verbatim}

The first line defines the $Time$ type that is equivalent to $nat$.
The function $f$ maps each cycle to time which builds the
correspondence between cycles and time. The method introducing time
into the model is different from that used in \cite{cg_Coq_PLC}. The
spans between two adjacent cycles are not always the same: the cycle
that executes more instructions costs more time. $f$ abstracts this
away. $t1\_value$ is the preset of $t1$ that is greater than $0$
which is stated by the hypothesis $t1\_LargerThan0$. The following
two hypothesis show the properties of this function and the relation
between it and the timer. The hypothesis $f\_monotonic$ expresses
that the time points of adjacent cycles increase strictly. The
hypothesis $f\_TimerLargerThanCycleInterval$ expresses that the
preset of $t1$ should be larger than the time interval between any
two adjacent cycles (this is required in practice). The first axiom
expresses that if the input of $t1$ (i.e. $m1$) turns OFF, then the
timer bit (i.e. $t1$) turns OFF immediately. The second axiom
expresses that if the input of $t1$ stays ON for a span longer than
$t1\_value$, then $t1$ turns ON immediately. The last axiom
expresses that if at cycle $c2$ $t1$ is ON then there exists a cycle
$c1$ such that the span between $c1$ and $c2$ is longer than
$t1\_value$ and $m1$ stays ON during this span.

\subsection{Preparation before the Modeling}

In the previous section we introduce some assumptions about the PLC
program. In this section, we introduce some other assumptions and
the method that modifies the original PLC to an equivalent one which
satisfies these assumptions.

First of all, we do not consider the programs that contains loops in
one cycle.

There are input relays, output relays and internal utility relays in
PLC. For input relays, PLC can only read their values, hence they
cannot be in the left hand side of assignments. There is a principle
in PLC design that the the value of an output relay can only be set
once in one cycle. So this kind of relays can be in the left hand
side of assignment only once. Internal utility relays are used to
record the internal states of PLC programs, and they can be set
multi-times in one cycle. If a PLC program has a internal relay set
twice in one cycle, then we  have two hypothesis like the following:

\begin{verbatim}
Hypothesis h_m8 : forall c, m8 c = m1 /\ m2.

Hypothesis h_m8 : forall c, m8 c = m1 \/ ~m2.
\end{verbatim}

This will make our model inconsistent, since there is a chance that
in a cycle these hypothesis make $m8$ have different values. There
several ways to solve this problem. The method we choose is
described as follows:

\begin{enumerate}

\item Go through the program from up to down, if a variable is found
that it has been set to some value already, then we choose an unused
name for it and rename it to the new name from that point on.

\item Repeat step 1 until there is no such variables.

\end{enumerate}

Since there is no loops inside one cycle and the variables used in a
program is finite, the process of the above steps terminates. It
also can be proved that the modified version is equivalent to the
original one and in the modified version each variable occurs in the
left hand side of the assignments at most once.

The TON-timers in S7-200 has three resolutions: $1ms$, $10ms$ and
$100ms$. Timers with different resolutions behave differently. The
last two kinds of timer are described in section
\ref{model_timer_section}. For the $1ms$ case, the timer updates
every $1ms$ asynchronous to the scan cycle. That means if we choose
this kind of timer to realize the quiz machine, the timer bit may
turn ON at any point during the scan cycle, which will make the
program treat plays unfairly. For instance, before the computation
phase the values of the relays are: $m1 = 1, m2 = m3 = m4 = m5=0,
i1=0, i2=i3=i4=1$ ($m1=1$ means the quiz machine was started, $m5
=0$ means there was no one pressed the button from the machine
stated to the previous cycle, $i2=1,i3=1$ and $i4=1$ means three
players pressed their buttons at the same time before the current
cycle). The time-out can happen at the points where the third and
fourth rung are executed. In the former case, the outputs are :
$o0=1, o1=o2=o3=0$. In the latter case, the output we have are :
$o0=o2=o3=0, o1=1$. This situation makes our model of computation
non-deterministic and also introduces unfair treatment to the
players. To solve this problem, we present the following solution:

\begin{itemize}

\item For the $10ms$ and $100ms$ cases, there is no need to modify
the program according to the design principle and semantics of
S7-200.

\item For the $1ms$ case, the access points of the value of a timer are the
instructions that refers to this value. It is enough to (given a
TON-timer $t1$ of $1ms$):

\begin{itemize}

\item If the number of instruction that refers to the value of $t1$ is one, then there is no need to do modification.

\item Insert a new assignment ``$m\_new := t1$'' ($m\_new$ is an
unused variable) before the first instruction referring to $t1$.

\item Rename all $t1$ to $m\_new$ in the instructions referring to $t1$.

\end{itemize}

\end{itemize}

\subsection{The Model of the Quiz Machine Program}

Based on the methods described in the previous sections, we have the
following model of the quiz machine program:

\begin{verbatim}
Variables i0 i1 i2 i3 i4 : Var.
Variables m1 m2 m3 m4 m5: Var.
Variables o0 o1 o2 o3 : Var.

Hypothesis h_m1 : forall c, m1 c =
   ((i0 c \/ m1 (pred c)) /\ ~ i1 c).

Hypothesis h_m2 : forall c, m2 c =
    (((m1 c /\ ~ t1 c /\ i2 c /\ ~ m5 (pred c)) \/ m2 (pred c)) /\ m1 c).

Hypothesis h_m3 : forall c, m3 c =
    (((m1 c /\ ~ t1 c /\ i3 c /\ ~ m5 (pred c)) \/ m3 (pred c)) /\ m1 c).

Hypothesis h_m4 : forall c, m4 c =
    (((m1 c /\ ~ t1 c /\ i4 c /\ ~ m5 (pred c)) \/ m4 (pred c)) /\ m1 c).

Hypothesis h_m5 : forall c, m5 c =
    (((m2 c \/ m3 c \/ m4 c) \/ m5 (pred c))/\ m1 c).

Hypothesis h_o1 : forall c, o1 c = m2 c.

Hypothesis h_o2 : forall c, o2 c = m3 c.

Hypothesis h_o3 : forall c, o3 c = m4 c.

Hypothesis h_o0 : forall c, o0 c = (t1 c /\ ~ m5 c).
\end{verbatim}

\section{Verification of Properties in Coq}

Before we present the theorems about the properties to proof, we
give some auxiliary definitions which make the representations more
clear.

\subsection{Auxiliary Definitions}

The comments above each definitions expresses the meanings of the
definitions.

\begin{verbatim}
%The host first presses the reset button, after a while he
%presses the start button.
Definition reset_then_start c1 c2 := c1 <= c2 /\ i1 c1 /\ i0 (S c2)
/\ being_false i0 c1 c2.

%The span between c1 and c2 is less than t1_value while the span
%between c1 and (S c2) (i.e. the cycle after c2) is larger than t1_value.
Definition just_time_out c1 c2 := t1_value <= f (S c2) - f c1 /\ f
c2 - f c1 < t1_value.

%Player p1 first presses his button.
Definition p1_first_presses c1 c2 := being_false i2 c1 (pred c2) /\
being_false i3 c1 c2 /\ being_false i4 c1 c2 /\ i2 c2.

%Player p1 and p2 press their button at the same time.
Definition p1p2_first_press c1 c2 := being_false i2 c1 (pred c2) /\
being_false i3 c1 (pred c2) /\ being_false i4 c1 c2 /\ i2 c2 /\ i3
c2.

%On one presses his button between c1 and c2.
Definition no_player_press c1 c2 := being_false i2 c1 c2 /\
being_false i3 c1 c2 /\ being_false i4 c1 c2.

%The reset button is not presses during c1 c2.
Definition not_reset c1 c2 := being_false i1 c1 c2.

%The variable o is false between c1 and (pred c2) and
%is true between c2 and c3.
Definition off_on o c1 c2 c3 := being_true o c2 c3 /\ being_false o
c1 (pred c2).

%The variable o stays off between c1 and c2.
Definition stay_off o c1 c2 := being_false o c1 c2.
\end{verbatim}

\subsection{Theorems of the Properties}

Here are the theorems we want to prove:

\begin{itemize}

\item
\begin{verbatim}
Theorem reset_start_time_i2_o0o1o2o3_f :
    forall c1 c2, reset_then_start c1 c2 ->
        forall c3,
            just_time_out (S c2) c3 ->
            forall c,
            S c2 <= c <= c3 -> p1_first_presses (S c2) c ->
            forall c4, c <= c4 ->
                not_reset (S c2) c4 ->
                stay_off o0 (S c2) c4 /\
                off_on o1 (S c2) c c4 /\
                stay_off o2 (S c2) c4 /\
                stay_off o3 (S c2) c4.
\end{verbatim}

\item
\begin{verbatim}
Theorem reset_start_time_i2i3_o0o1o2o3_f :
    forall c1 c2, reset_then_start c1 c2 ->
        forall c3,
            just_time_out (S c2) c3 ->
            forall c,
            S c2 <= c <= c3 ->
            p1p2_first_press (S c2) c ->
            forall c4, c <= c4 ->
                not_reset (S c2) c4 ->
                stay_off o0 (S c2) c4 /\
                off_on o1 (S c2) c c4 /\
                off_on o2 (S c2) c c4 /\
                stay_off o3 (S c2) c4.
\end{verbatim}

\item
\begin{verbatim}
Theorem reset_start_exceed_time_o0o1o2o3_f :
    forall c1 c2, reset_then_start c1 c2 ->
        forall c3,
            just_time_out (S c2) c3 ->
            no_player_press (S c2) c3 ->
            forall c4, S c3 <= c4 ->
                not_reset (S c2) c4 ->
                off_on o0 (S c2) (S c3) c4 /\
                stay_off o1 (S c2) c4 /\
                stay_off o2 (S c2) c4 /\
                stay_off o3 (S c2) c4.
\end{verbatim}

\end{itemize}

Take the first theorem for example, the formulae before the last
arrow present the premises, i.e. the behaviors of the environment
(including the actions of the people); those after the last arrow
describe the conclusions, i.e. the expected behavior of the system.
Figure \ref{fig_theorem_1} is a graphic representation of theorem 1,
where the words in normal form describe the premises and the words
in italic describe conclusions. The host presses reset button at
$c1$ and doesn't press start button from $c1$ to $c2$. Then he
presses start button at $S ~c2$ (i.e. the next cycle of $c2$). The
time span between $S ~c2$ and $c3$ is less than $t1\_value$ and that
between $S ~c2$ and $S ~c3$ is equal or larger than $t1\_value$.
There exists a cycle $c$ such that during $S~ c2$ and $pred ~c$
(i.e. the previous cycle of $c$) no one presses his button and at
$c$ only player 1 presses his button which means player 1 is first
one who first presses the button before the time-out. During $S~c2$
and $c4$ the reset button is not pressed. The conclusion shows that
during $S~c2$ and $pred~c$ the light 1 is off and during $c$ and
$c4$ the light 1 is on; during $S c2$ and $c4$ the lights 0, 2 and 3
are all off.


\begin{figure}[]
        \includegraphics[scale = 0.72]
        {figs/fig_theorem_1}
        \caption{\label{fig_theorem_1}Graphic representation of theorem 1}
      \end{figure}

\subsection{Outline of the Proof}

Since the proofs of the three theorems are lengthy -- the whole file
has 2562 lines -- we only outline the proof idea here.

The model of the quiz machine can be understood as a transition
system.  The state of the system is an vector consisting of all the
internal relays : ($m1,m2,m3,m4,m5$). The inputs of the program,
i.e. $i0,i1,i2,i3,i4$, and the time-out signal are the guard on the
transitions. Part of transition system used to prove theorem 1 is
demonstrated in figure \ref{fig_quizm_trans}. The numbers in the
states above the line indicate the values of $m1,m2,m3,m4$, and $m5$
respectively and those below the line indicate the values of
$o0,o1,o2$,and $o3$. The variables above the transitions represent
the conditions under which the corresponding transition can take
place. Variables not mentioned means the transition does not care
the values of these variables. For instance, if the system is at
state $s1$, then all the output and internal relays are all $0$. If
$i0$ is false, whatever values other variable are the system stays
in $s1$. If $i$ is true, then the state changes to $s2$.

The promises of theorem 1 represent the inputs of the system and
their orders:

\begin{enumerate}

\item The host presses the reset button.

\item The host presses the start button and does not press the reset button afterwards.

\item Player 1 firstly presses his button.

\end{enumerate}

We proved that following these inputs, the system

\begin{itemize}

\item reaches $s1$ after the host presses the reset button; then

\item it reaches $s2$ after the host presses the start button; then

\item it reaches $s3$ after player 1 presses his button before
time-out.

\end{itemize}

And the outputs of this process coincide with the conclusion of
theorem 1.

The other two theorems are proved in the same manner.


\begin{figure}[]
        \includegraphics[scale = 0.72]
        {figs/QuizMachine_transition}
        \caption{\label{fig_quizm_trans}A part of the transition system}
      \end{figure}

\section{Conclusions}

\bibliographystyle{splncs}
\bibliography{ref}

\end{document}
